Termination w.r.t. Q proof of TRS/HMt009.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

Q is empty.

↳ QTRS

  ↳ AAECC Innermost

Q restricted rewrite system:
The TRS R consists of the following rules:

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

Q is empty.

We have applied [15,7] to switch to innermost. The TRS R 1 is

or(true, b) → true
or(false, b) → b

The TRS R 2 is

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)

The signature Sigma is {idle, start, incorrect, busy, correct}

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

The set Q consists of the following terms:

start(x0)
busy(BF, x0, stop, x1, x2, x3, x4)
busy(FS, x0, stop, x1, x2, x3, x4)
busy(x0, open, up, x1, x2, x3, x4)
busy(x0, open, down, x1, x2, x3, x4)
busy(B, closed, stop, false, false, false, empty)
busy(F, closed, stop, false, false, false, empty)
busy(S, closed, stop, false, false, false, empty)
busy(B, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(F, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(S, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(B, open, stop, false, x0, x1, x2)
busy(F, open, stop, x0, false, x1, x2)
busy(S, open, stop, x0, x1, false, x2)
busy(B, x0, stop, true, x1, x2, x3)
busy(F, x0, stop, x1, true, x2, x3)
busy(S, x0, stop, x1, x2, true, x3)
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
idle(x0, x1, x2, x3, x4, x5, newbuttons(x6, x7, x8, x9))
or(true, x0)
or(false, x0)

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → BUSY(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
BUSY(B, open, stop, false, b2, b3, i) → IDLE(B, closed, stop, false, b2, b3, i)
BUSY(S, d, stop, b1, b2, true, i) → IDLE(S, open, stop, b1, b2, false, i)
BUSY(F, open, stop, b1, false, b3, i) → IDLE(F, closed, stop, b1, false, b3, i)
BUSY(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, open, stop, b1, b2, false, i) → IDLE(S, closed, stop, b1, b2, false, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
IDLE(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → OR(b3, i3)
START(i) → BUSY(F, closed, stop, false, false, false, i)
IDLE(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → OR(b2, i2)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
BUSY(F, d, stop, b1, true, b3, i) → IDLE(F, open, stop, b1, false, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
IDLE(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → OR(b1, i1)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(B, d, stop, true, b2, b3, i) → IDLE(B, open, stop, false, b2, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)

The TRS R consists of the following rules:

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

The set Q consists of the following terms:

start(x0)
busy(BF, x0, stop, x1, x2, x3, x4)
busy(FS, x0, stop, x1, x2, x3, x4)
busy(x0, open, up, x1, x2, x3, x4)
busy(x0, open, down, x1, x2, x3, x4)
busy(B, closed, stop, false, false, false, empty)
busy(F, closed, stop, false, false, false, empty)
busy(S, closed, stop, false, false, false, empty)
busy(B, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(F, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(S, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(B, open, stop, false, x0, x1, x2)
busy(F, open, stop, x0, false, x1, x2)
busy(S, open, stop, x0, x1, false, x2)
busy(B, x0, stop, true, x1, x2, x3)
busy(F, x0, stop, x1, true, x2, x3)
busy(S, x0, stop, x1, x2, true, x3)
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
idle(x0, x1, x2, x3, x4, x5, newbuttons(x6, x7, x8, x9))
or(true, x0)
or(false, x0)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

Q DP problem:
The TRS P consists of the following rules:

BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → BUSY(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
BUSY(B, open, stop, false, b2, b3, i) → IDLE(B, closed, stop, false, b2, b3, i)
BUSY(S, d, stop, b1, b2, true, i) → IDLE(S, open, stop, b1, b2, false, i)
BUSY(F, open, stop, b1, false, b3, i) → IDLE(F, closed, stop, b1, false, b3, i)
BUSY(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, open, stop, b1, b2, false, i) → IDLE(S, closed, stop, b1, b2, false, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
IDLE(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → OR(b3, i3)
START(i) → BUSY(F, closed, stop, false, false, false, i)
IDLE(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → OR(b2, i2)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
BUSY(F, d, stop, b1, true, b3, i) → IDLE(F, open, stop, b1, false, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
IDLE(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → OR(b1, i1)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(B, d, stop, true, b2, b3, i) → IDLE(B, open, stop, false, b2, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)

The TRS R consists of the following rules:

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

The set Q consists of the following terms:

start(x0)
busy(BF, x0, stop, x1, x2, x3, x4)
busy(FS, x0, stop, x1, x2, x3, x4)
busy(x0, open, up, x1, x2, x3, x4)
busy(x0, open, down, x1, x2, x3, x4)
busy(B, closed, stop, false, false, false, empty)
busy(F, closed, stop, false, false, false, empty)
busy(S, closed, stop, false, false, false, empty)
busy(B, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(F, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(S, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(B, open, stop, false, x0, x1, x2)
busy(F, open, stop, x0, false, x1, x2)
busy(S, open, stop, x0, x1, false, x2)
busy(B, x0, stop, true, x1, x2, x3)
busy(F, x0, stop, x1, true, x2, x3)
busy(S, x0, stop, x1, x2, true, x3)
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
idle(x0, x1, x2, x3, x4, x5, newbuttons(x6, x7, x8, x9))
or(true, x0)
or(false, x0)

We have to consider all minimal (P,Q,R)-chains.
We deleted some edges using various graph approximations

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → BUSY(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
BUSY(B, open, stop, false, b2, b3, i) → IDLE(B, closed, stop, false, b2, b3, i)
BUSY(S, d, stop, b1, b2, true, i) → IDLE(S, open, stop, b1, b2, false, i)
BUSY(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
BUSY(F, open, stop, b1, false, b3, i) → IDLE(F, closed, stop, b1, false, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(S, open, stop, b1, b2, false, i) → IDLE(S, closed, stop, b1, b2, false, i)
START(i) → BUSY(F, closed, stop, false, false, false, i)
IDLE(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → OR(b3, i3)
IDLE(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → OR(b2, i2)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
BUSY(F, d, stop, b1, true, b3, i) → IDLE(F, open, stop, b1, false, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
IDLE(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → OR(b1, i1)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(B, d, stop, true, b2, b3, i) → IDLE(B, open, stop, false, b2, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)

The TRS R consists of the following rules:

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

The set Q consists of the following terms:

start(x0)
busy(BF, x0, stop, x1, x2, x3, x4)
busy(FS, x0, stop, x1, x2, x3, x4)
busy(x0, open, up, x1, x2, x3, x4)
busy(x0, open, down, x1, x2, x3, x4)
busy(B, closed, stop, false, false, false, empty)
busy(F, closed, stop, false, false, false, empty)
busy(S, closed, stop, false, false, false, empty)
busy(B, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(F, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(S, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(B, open, stop, false, x0, x1, x2)
busy(F, open, stop, x0, false, x1, x2)
busy(S, open, stop, x0, x1, false, x2)
busy(B, x0, stop, true, x1, x2, x3)
busy(F, x0, stop, x1, true, x2, x3)
busy(S, x0, stop, x1, x2, true, x3)
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
idle(x0, x1, x2, x3, x4, x5, newbuttons(x6, x7, x8, x9))
or(true, x0)
or(false, x0)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 1 SCC with 4 less nodes.

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ QDP

                  ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → BUSY(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
BUSY(B, open, stop, false, b2, b3, i) → IDLE(B, closed, stop, false, b2, b3, i)
BUSY(S, d, stop, b1, b2, true, i) → IDLE(S, open, stop, b1, b2, false, i)
BUSY(F, open, stop, b1, false, b3, i) → IDLE(F, closed, stop, b1, false, b3, i)
BUSY(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, open, stop, b1, b2, false, i) → IDLE(S, closed, stop, b1, b2, false, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
BUSY(F, d, stop, b1, true, b3, i) → IDLE(F, open, stop, b1, false, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(B, d, stop, true, b2, b3, i) → IDLE(B, open, stop, false, b2, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)

The TRS R consists of the following rules:

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

The set Q consists of the following terms:

start(x0)
busy(BF, x0, stop, x1, x2, x3, x4)
busy(FS, x0, stop, x1, x2, x3, x4)
busy(x0, open, up, x1, x2, x3, x4)
busy(x0, open, down, x1, x2, x3, x4)
busy(B, closed, stop, false, false, false, empty)
busy(F, closed, stop, false, false, false, empty)
busy(S, closed, stop, false, false, false, empty)
busy(B, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(F, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(S, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(B, open, stop, false, x0, x1, x2)
busy(F, open, stop, x0, false, x1, x2)
busy(S, open, stop, x0, x1, false, x2)
busy(B, x0, stop, true, x1, x2, x3)
busy(F, x0, stop, x1, true, x2, x3)
busy(S, x0, stop, x1, x2, true, x3)
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
idle(x0, x1, x2, x3, x4, x5, newbuttons(x6, x7, x8, x9))
or(true, x0)
or(false, x0)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

IDLE(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → BUSY(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)

The remaining pairs can at least be oriented weakly.

BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(B, open, stop, false, b2, b3, i) → IDLE(B, closed, stop, false, b2, b3, i)
BUSY(S, d, stop, b1, b2, true, i) → IDLE(S, open, stop, b1, b2, false, i)
BUSY(F, open, stop, b1, false, b3, i) → IDLE(F, closed, stop, b1, false, b3, i)
BUSY(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, open, stop, b1, b2, false, i) → IDLE(S, closed, stop, b1, b2, false, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
BUSY(F, d, stop, b1, true, b3, i) → IDLE(F, open, stop, b1, false, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(B, d, stop, true, b2, b3, i) → IDLE(B, open, stop, false, b2, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)

Used ordering: Combined order from the following AFS and order.
BUSY(x1, x2, x3, x4, x5, x6, x7) = x7
S = S
closed = closed
stop = stop
true = true
false = false
IDLE(x1, x2, x3, x4, x5, x6, x7) = x7
down = down
newbuttons(x1, x2, x3, x4) = newbuttons(x2, x4)
or(x1, x2) = or(x1, x2)
B = B
open = open
F = F
up = up
BF = BF
FS = FS
empty = empty

Lexicographic Path Order [19].
Precedence:

stop > closed > newbuttons₂ > S > false > down > B > true > empty
stop > closed > newbuttons₂ > S > false > down > B > open > empty
stop > closed > newbuttons₂ > S > false > down > B > BF > empty
stop > closed > newbuttons₂ > S > false > down > F > true > empty
stop > closed > newbuttons₂ > S > false > down > F > open > empty
stop > closed > newbuttons₂ > S > false > down > F > BF > empty
stop > closed > newbuttons₂ > or₂ > true > empty
stop > closed > FS > up > false > down > B > true > empty
stop > closed > FS > up > false > down > B > open > empty
stop > closed > FS > up > false > down > B > BF > empty
stop > closed > FS > up > false > down > F > true > empty
stop > closed > FS > up > false > down > F > open > empty
stop > closed > FS > up > false > down > F > BF > empty

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ QDP

                  ↳ QDPOrderProof

                    ↳ QDP

                      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(B, open, stop, false, b2, b3, i) → IDLE(B, closed, stop, false, b2, b3, i)
BUSY(S, d, stop, b1, b2, true, i) → IDLE(S, open, stop, b1, b2, false, i)
BUSY(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
BUSY(F, open, stop, b1, false, b3, i) → IDLE(F, closed, stop, b1, false, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(S, open, stop, b1, b2, false, i) → IDLE(S, closed, stop, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
BUSY(F, d, stop, b1, true, b3, i) → IDLE(F, open, stop, b1, false, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(B, d, stop, true, b2, b3, i) → IDLE(B, open, stop, false, b2, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)

The TRS R consists of the following rules:

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

The set Q consists of the following terms:

start(x0)
busy(BF, x0, stop, x1, x2, x3, x4)
busy(FS, x0, stop, x1, x2, x3, x4)
busy(x0, open, up, x1, x2, x3, x4)
busy(x0, open, down, x1, x2, x3, x4)
busy(B, closed, stop, false, false, false, empty)
busy(F, closed, stop, false, false, false, empty)
busy(S, closed, stop, false, false, false, empty)
busy(B, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(F, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(S, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(B, open, stop, false, x0, x1, x2)
busy(F, open, stop, x0, false, x1, x2)
busy(S, open, stop, x0, x1, false, x2)
busy(B, x0, stop, true, x1, x2, x3)
busy(F, x0, stop, x1, true, x2, x3)
busy(S, x0, stop, x1, x2, true, x3)
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
idle(x0, x1, x2, x3, x4, x5, newbuttons(x6, x7, x8, x9))
or(true, x0)
or(false, x0)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 1 SCC with 3 less nodes.

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ QDP

                  ↳ QDPOrderProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(B, open, stop, false, b2, b3, i) → IDLE(B, closed, stop, false, b2, b3, i)
BUSY(S, d, stop, b1, b2, true, i) → IDLE(S, open, stop, b1, b2, false, i)
BUSY(F, open, stop, b1, false, b3, i) → IDLE(F, closed, stop, b1, false, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, open, stop, b1, b2, false, i) → IDLE(S, closed, stop, b1, b2, false, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(F, d, stop, b1, true, b3, i) → IDLE(F, open, stop, b1, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(B, d, stop, true, b2, b3, i) → IDLE(B, open, stop, false, b2, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)

The TRS R consists of the following rules:

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

The set Q consists of the following terms:

start(x0)
busy(BF, x0, stop, x1, x2, x3, x4)
busy(FS, x0, stop, x1, x2, x3, x4)
busy(x0, open, up, x1, x2, x3, x4)
busy(x0, open, down, x1, x2, x3, x4)
busy(B, closed, stop, false, false, false, empty)
busy(F, closed, stop, false, false, false, empty)
busy(S, closed, stop, false, false, false, empty)
busy(B, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(F, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(S, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(B, open, stop, false, x0, x1, x2)
busy(F, open, stop, x0, false, x1, x2)
busy(S, open, stop, x0, x1, false, x2)
busy(B, x0, stop, true, x1, x2, x3)
busy(F, x0, stop, x1, true, x2, x3)
busy(S, x0, stop, x1, x2, true, x3)
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
idle(x0, x1, x2, x3, x4, x5, newbuttons(x6, x7, x8, x9))
or(true, x0)
or(false, x0)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

BUSY(B, d, stop, true, b2, b3, i) → IDLE(B, open, stop, false, b2, b3, i)

The remaining pairs can at least be oriented weakly.

BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(B, open, stop, false, b2, b3, i) → IDLE(B, closed, stop, false, b2, b3, i)
BUSY(S, d, stop, b1, b2, true, i) → IDLE(S, open, stop, b1, b2, false, i)
BUSY(F, open, stop, b1, false, b3, i) → IDLE(F, closed, stop, b1, false, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, open, stop, b1, b2, false, i) → IDLE(S, closed, stop, b1, b2, false, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(F, d, stop, b1, true, b3, i) → IDLE(F, open, stop, b1, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)

Used ordering: Combined order from the following AFS and order.
BUSY(x1, x2, x3, x4, x5, x6, x7) = x4
S = S
closed = closed
stop = stop
true = true
false = false
IDLE(x1, x2, x3, x4, x5, x6, x7) = x4
down = down
B = B
open = open
F = F
up = up
BF = BF
FS = FS
empty = empty

Lexicographic Path Order [19].
Precedence:

stop > true > down > S > closed
stop > true > down > false > F > closed
stop > true > down > false > up > B > closed
stop > open > S > closed
stop > open > false > F > closed
stop > open > false > up > B > closed
BF > down > S > closed
BF > down > false > F > closed
BF > down > false > up > B > closed
FS > S > closed
FS > F > closed
FS > up > B > closed
empty > closed

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ QDP

                  ↳ QDPOrderProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ QDPOrderProof

                            ↳ QDP

                              ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(B, open, stop, false, b2, b3, i) → IDLE(B, closed, stop, false, b2, b3, i)
BUSY(S, d, stop, b1, b2, true, i) → IDLE(S, open, stop, b1, b2, false, i)
BUSY(F, open, stop, b1, false, b3, i) → IDLE(F, closed, stop, b1, false, b3, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(S, open, stop, b1, b2, false, i) → IDLE(S, closed, stop, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(F, d, stop, b1, true, b3, i) → IDLE(F, open, stop, b1, false, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)

The TRS R consists of the following rules:

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

The set Q consists of the following terms:

start(x0)
busy(BF, x0, stop, x1, x2, x3, x4)
busy(FS, x0, stop, x1, x2, x3, x4)
busy(x0, open, up, x1, x2, x3, x4)
busy(x0, open, down, x1, x2, x3, x4)
busy(B, closed, stop, false, false, false, empty)
busy(F, closed, stop, false, false, false, empty)
busy(S, closed, stop, false, false, false, empty)
busy(B, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(F, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(S, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(B, open, stop, false, x0, x1, x2)
busy(F, open, stop, x0, false, x1, x2)
busy(S, open, stop, x0, x1, false, x2)
busy(B, x0, stop, true, x1, x2, x3)
busy(F, x0, stop, x1, true, x2, x3)
busy(S, x0, stop, x1, x2, true, x3)
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
idle(x0, x1, x2, x3, x4, x5, newbuttons(x6, x7, x8, x9))
or(true, x0)
or(false, x0)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

BUSY(F, d, stop, b1, true, b3, i) → IDLE(F, open, stop, b1, false, b3, i)

The remaining pairs can at least be oriented weakly.

BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(B, open, stop, false, b2, b3, i) → IDLE(B, closed, stop, false, b2, b3, i)
BUSY(S, d, stop, b1, b2, true, i) → IDLE(S, open, stop, b1, b2, false, i)
BUSY(F, open, stop, b1, false, b3, i) → IDLE(F, closed, stop, b1, false, b3, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(S, open, stop, b1, b2, false, i) → IDLE(S, closed, stop, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)

Used ordering: Combined order from the following AFS and order.
BUSY(x1, x2, x3, x4, x5, x6, x7) = x5
S = S
closed = closed
stop = stop
true = true
false = false
IDLE(x1, x2, x3, x4, x5, x6, x7) = x5
down = down
B = B
open = open
F = F
up = up
BF = BF
FS = FS
empty = empty

Lexicographic Path Order [19].
Precedence:

stop > S > true > open > false
stop > S > true > open > F
stop > S > down > false
stop > S > down > F
stop > closed > down > false
stop > closed > down > F
stop > closed > B > true > open > false
stop > closed > B > true > open > F
stop > closed > up > true > open > false
stop > closed > up > true > open > F
BF > closed > down > false
BF > closed > down > F
BF > closed > B > true > open > false
BF > closed > B > true > open > F
BF > closed > up > true > open > false
BF > closed > up > true > open > F
FS > S > true > open > false
FS > S > true > open > F
FS > S > down > false
FS > S > down > F
FS > closed > down > false
FS > closed > down > F
FS > closed > B > true > open > false
FS > closed > B > true > open > F
FS > closed > up > true > open > false
FS > closed > up > true > open > F

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ QDP

                  ↳ QDPOrderProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ QDPOrderProof

                            ↳ QDP

                              ↳ QDPOrderProof

                                ↳ QDP

                                  ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(B, open, stop, false, b2, b3, i) → IDLE(B, closed, stop, false, b2, b3, i)
BUSY(S, d, stop, b1, b2, true, i) → IDLE(S, open, stop, b1, b2, false, i)
BUSY(F, open, stop, b1, false, b3, i) → IDLE(F, closed, stop, b1, false, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, open, stop, b1, b2, false, i) → IDLE(S, closed, stop, b1, b2, false, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)

The TRS R consists of the following rules:

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

The set Q consists of the following terms:

start(x0)
busy(BF, x0, stop, x1, x2, x3, x4)
busy(FS, x0, stop, x1, x2, x3, x4)
busy(x0, open, up, x1, x2, x3, x4)
busy(x0, open, down, x1, x2, x3, x4)
busy(B, closed, stop, false, false, false, empty)
busy(F, closed, stop, false, false, false, empty)
busy(S, closed, stop, false, false, false, empty)
busy(B, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(F, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(S, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(B, open, stop, false, x0, x1, x2)
busy(F, open, stop, x0, false, x1, x2)
busy(S, open, stop, x0, x1, false, x2)
busy(B, x0, stop, true, x1, x2, x3)
busy(F, x0, stop, x1, true, x2, x3)
busy(S, x0, stop, x1, x2, true, x3)
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
idle(x0, x1, x2, x3, x4, x5, newbuttons(x6, x7, x8, x9))
or(true, x0)
or(false, x0)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

BUSY(S, d, stop, b1, b2, true, i) → IDLE(S, open, stop, b1, b2, false, i)

The remaining pairs can at least be oriented weakly.

BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(B, open, stop, false, b2, b3, i) → IDLE(B, closed, stop, false, b2, b3, i)
BUSY(F, open, stop, b1, false, b3, i) → IDLE(F, closed, stop, b1, false, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, open, stop, b1, b2, false, i) → IDLE(S, closed, stop, b1, b2, false, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)

Used ordering: Combined order from the following AFS and order.
BUSY(x1, x2, x3, x4, x5, x6, x7) = x6
S = S
closed = closed
stop = stop
true = true
false = false
IDLE(x1, x2, x3, x4, x5, x6, x7) = x6
down = down
B = B
open = open
F = F
up = up
BF = BF
FS = FS
empty = empty

Lexicographic Path Order [19].
Precedence:

closed > stop > S > true > false
closed > stop > S > open > false
closed > stop > B > true > false
closed > stop > B > BF > false
closed > stop > F > true > false
closed > stop > F > BF > false
closed > down > S > true > false
closed > down > S > open > false
closed > down > B > true > false
closed > down > B > BF > false
closed > down > F > true > false
closed > down > F > BF > false
closed > down > FS > false
closed > up > S > true > false
closed > up > S > open > false
closed > up > B > true > false
closed > up > B > BF > false
closed > up > F > true > false
closed > up > F > BF > false
closed > up > FS > false
empty > false

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ QDP

                  ↳ QDPOrderProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ QDPOrderProof

                            ↳ QDP

                              ↳ QDPOrderProof

                                ↳ QDP

                                  ↳ QDPOrderProof

                                    ↳ QDP

                                      ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, open, stop, false, b2, b3, i) → IDLE(B, closed, stop, false, b2, b3, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, open, stop, b1, false, b3, i) → IDLE(F, closed, stop, b1, false, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, open, stop, b1, b2, false, i) → IDLE(S, closed, stop, b1, b2, false, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)

The TRS R consists of the following rules:

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

The set Q consists of the following terms:

start(x0)
busy(BF, x0, stop, x1, x2, x3, x4)
busy(FS, x0, stop, x1, x2, x3, x4)
busy(x0, open, up, x1, x2, x3, x4)
busy(x0, open, down, x1, x2, x3, x4)
busy(B, closed, stop, false, false, false, empty)
busy(F, closed, stop, false, false, false, empty)
busy(S, closed, stop, false, false, false, empty)
busy(B, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(F, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(S, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(B, open, stop, false, x0, x1, x2)
busy(F, open, stop, x0, false, x1, x2)
busy(S, open, stop, x0, x1, false, x2)
busy(B, x0, stop, true, x1, x2, x3)
busy(F, x0, stop, x1, true, x2, x3)
busy(S, x0, stop, x1, x2, true, x3)
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
idle(x0, x1, x2, x3, x4, x5, newbuttons(x6, x7, x8, x9))
or(true, x0)
or(false, x0)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

BUSY(B, open, stop, false, b2, b3, i) → IDLE(B, closed, stop, false, b2, b3, i)
BUSY(F, open, stop, b1, false, b3, i) → IDLE(F, closed, stop, b1, false, b3, i)
BUSY(S, open, stop, b1, b2, false, i) → IDLE(S, closed, stop, b1, b2, false, i)

The remaining pairs can at least be oriented weakly.

BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)

Used ordering: Combined order from the following AFS and order.
BUSY(x1, x2, x3, x4, x5, x6, x7) = x2
S = S
closed = closed
stop = stop
true = true
false = false
IDLE(x1, x2, x3, x4, x5, x6, x7) = x2
down = down
B = B
up = up
F = F
BF = BF
FS = FS
open = open
empty = empty

Lexicographic Path Order [19].
Precedence:

false > S > down > true > up > stop > closed
false > B > true > up > stop > closed
false > F > BF > down > true > up > stop > closed
FS > S > down > true > up > stop > closed
FS > F > BF > down > true > up > stop > closed
open > closed
empty > closed

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ QDP

                  ↳ QDPOrderProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ QDPOrderProof

                            ↳ QDP

                              ↳ QDPOrderProof

                                ↳ QDP

                                  ↳ QDPOrderProof

                                    ↳ QDP

                                      ↳ QDPOrderProof

                                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)

The TRS R consists of the following rules:

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

The set Q consists of the following terms:

start(x0)
busy(BF, x0, stop, x1, x2, x3, x4)
busy(FS, x0, stop, x1, x2, x3, x4)
busy(x0, open, up, x1, x2, x3, x4)
busy(x0, open, down, x1, x2, x3, x4)
busy(B, closed, stop, false, false, false, empty)
busy(F, closed, stop, false, false, false, empty)
busy(S, closed, stop, false, false, false, empty)
busy(B, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(F, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(S, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(B, open, stop, false, x0, x1, x2)
busy(F, open, stop, x0, false, x1, x2)
busy(S, open, stop, x0, x1, false, x2)
busy(B, x0, stop, true, x1, x2, x3)
busy(F, x0, stop, x1, true, x2, x3)
busy(S, x0, stop, x1, x2, true, x3)
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
idle(x0, x1, x2, x3, x4, x5, newbuttons(x6, x7, x8, x9))
or(true, x0)
or(false, x0)

We have to consider all minimal (P,Q,R)-chains.